1 /-
2 Copyright (c) 2018 Patrick Massot. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Patrick Massot, Johannes Hölzl
5
6 Continuous linear functions -- functions between normed vector spaces which are bounded and linear.
7 -/
8 import algebra.field
src └───────────┘
9 import analysis.normed_space.operator_norm
src └─────────────────────────────────┘
10
11 noncomputable theory
12 open_locale classical filter
13
14 open filter (tendsto)
15 open metric
16
17 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
18 variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
19 variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
20 variables {G : Type*} [normed_group G] [normed_space 𝕜 G]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
21
22 set_option class.instance_max_depth 70
doc └──────────────────────┘
23
24 /-- A function `f` satisfies `is_bounded_linear_map 𝕜 f` if it is linear and satisfies the
25 inequality `∥ f x ∥ ≤ M * ∥ x ∥` for some positive constant `M`. -/
26 structure is_bounded_linear_map (𝕜 : Type*) [normed_field 𝕜]
27 {E : Type*} [normed_group E] [normed_space 𝕜 E]
28 {F : Type*} [normed_group F] [normed_space 𝕜 F] (f : E → F)
29 extends is_linear_map 𝕜 f : Prop :=
30 (bound : ∃ M, 0 < M ∧ ∀ x : E, ∥ f x ∥ ≤ M * ∥ x ∥)
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
31
32 lemma is_linear_map.with_bound
33 {f : E → F} (hf : is_linear_map 𝕜 f) (M : ℝ) (h : ∀ x : E, ∥ f x ∥ ≤ M * ∥ x ∥) :
id ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
34 is_bounded_linear_map 𝕜 f :=
id └───────────────────┘ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴
doc └───────────────────┘
35 ⟨ hf, classical.by_cases
id └┘ └────────────────┘
src └────────────────┘
typ └┘ └────────────────┘
36 (assume : M ≤ 0, ⟨1, zero_lt_one, assume x,
id ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘
typ ┴ ┴ └─────────┘ ┴
37 le_trans (h x) $ mul_le_mul_of_nonneg_right (le_trans this zero_le_one) (norm_nonneg x)⟩)
id └──────┘ ┴ ┴ └────────────────────────┘ └──────┘ └──┘ └─────────┘ └─────────┘ ┴
src └──────┘ └────────────────────────┘ └──────┘ └─────────┘ └─────────┘
typ └──────┘ ┴ ┴ └────────────────────────┘ └──────┘ └──┘ └─────────┘ └─────────┘ ┴
38 (assume : ¬ M ≤ 0, ⟨M, lt_of_not_ge this, h⟩)⟩
id ┴ ┴ ┴ ┴ └──────────┘ └──┘ ┴
src ┴ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ └──────────┘ └──┘ ┴
39
40 /-- A continuous linear map satisfies `is_bounded_linear_map` -/
41 lemma continuous_linear_map.is_bounded_linear_map (f : E →L[𝕜] F) : is_bounded_linear_map 𝕜 f :=
id ┴ └─┘┴┴ ┴ └───────────────────┘ ┴ ┴
src └─┘ ┴ └───────────────────┘
typ ┴ └─┘┴┴ ┴ └───────────────────┘ ┴ ┴
doc └─┘ ┴ └───────────────────┘
42 { bound := f.bound,
id ┴└────┘
src └────┘
typ ┴└────┘
43 ..f.to_linear_map }
id ┴└────────────┘
src └────────────┘
typ ┴└────────────┘
44
45 namespace is_bounded_linear_map
46
47 /-- Construct a linear map from a function `f` satisfying `is_bounded_linear_map 𝕜 f`. -/
48 def to_linear_map (f : E → F) (h : is_bounded_linear_map 𝕜 f) : E →ₗ[𝕜] F :=
id ┴ ┴ └───────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
src └───────────────────┘ └─┘ ┴
typ ┴ ┴ └───────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
doc └───────────────────┘
49 (is_linear_map.mk' _ h.to_is_linear_map)
id └───────────────┘ ┴└───────────────┘
src └───────────────┘ └───────────────┘
typ └───────────────┘ ┴└───────────────┘
50
51 /-- Construct a continuous linear map from is_bounded_linear_map -/
52 def to_continuous_linear_map {f : E → F} (hf : is_bounded_linear_map 𝕜 f) : E →L[𝕜] F :=
id ┴ ┴ └───────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
src └───────────────────┘ └─┘ ┴
typ ┴ ┴ └───────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴
doc └───────────────────┘ └─┘ ┴
53 { cont := let ⟨C, Cpos, hC⟩ := hf.bound in linear_map.continuous_of_bound _ C hC,
id └─┘ ┴ └┘ └┘└────┘ └────────────────────────────┘
src └────┘ └────────────────────────────┘
typ └─┘ ┴ └┘ └┘└────┘ └────────────────────────────┘
54 ..to_linear_map f hf}
id └───────────┘ ┴ └┘
src └───────────┘
typ └───────────┘ ┴ └┘
doc └───────────┘
55
56 lemma zero : is_bounded_linear_map 𝕜 (λ (x:E), (0:F)) :=
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
57 (0 : E →ₗ F).is_linear.with_bound 0 $ by simp [le_refl]
id ┴ └┘ ┴ └───────┘ └────────┘ └─────┘
src └┘ └───────┘ └────────┘ └────┘└─────┘└─
typ ┴ └┘ ┴ └───────┘ └────────┘ └────┘└─────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────
58
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
59 lemma id : is_bounded_linear_map 𝕜 (λ (x:E), x) :=
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
60 linear_map.id.is_linear.with_bound 1 $ by simp [le_refl]
id └───────────┘└────────┘└─────────┘ └─────┘
src └───────────┘└────────┘└─────────┘ └────┘└─────┘└─
typ └───────────┘└────────┘└─────────┘ └────┘└─────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────
61
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
62 lemma fst : is_bounded_linear_map 𝕜 (λ x : E × F, x.1) :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴┴
src └───────────────────┘ ┴ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴┴
doc └───────────────────┘
63 begin
st └─────
64 refine (linear_map.fst 𝕜 E F).is_linear.with_bound 1 (λx, _),
id └────────────┘ ┴ ┴ ┴
src └─────┘ └────────────┘┴ ┴ ┴ └───────────────────────┘ └───┘
typ └─────┘ └────────────┘┴┴┴┴┴┴└───────────────────────┘ └───┘
doc └─────┘ └────────────┘┴ ┴ ┴ └───────────────────────┘ └───┘
txt └─────┘ ┴ ┴ ┴ └───────────────────────┘ └───┘
par └─────┘ ┴ ┴ ┴ └───────────────────────┘ └───┘
pid ┴ ┴ ┴ ┴ └───────────────────────┘ └───┘
st ─────────────────────────────────────────────────────────────┘└─
65 rw one_mul,
id └─────┘
src └─┘└─────┘
typ └─┘└─────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────┘└─
66 exact le_max_left _ _
id └─────────┘
src └────┘└─────────┘└───┘
typ └────┘└─────────┘└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └──┘┴
st ───────────────────────┘
67 end
st └─┘
68
69 lemma snd : is_bounded_linear_map 𝕜 (λ x : E × F, x.2) :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴┴
src └───────────────────┘ ┴ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴┴
doc └───────────────────┘
70 begin
st └─────
71 refine (linear_map.snd 𝕜 E F).is_linear.with_bound 1 (λx, _),
id └────────────┘ ┴ ┴ ┴
src └─────┘ └────────────┘┴ ┴ ┴ └───────────────────────┘ └───┘
typ └─────┘ └────────────┘┴┴┴┴┴┴└───────────────────────┘ └───┘
doc └─────┘ └────────────┘┴ ┴ ┴ └───────────────────────┘ └───┘
txt └─────┘ ┴ ┴ ┴ └───────────────────────┘ └───┘
par └─────┘ ┴ ┴ ┴ └───────────────────────┘ └───┘
pid ┴ ┴ ┴ ┴ └───────────────────────┘ └───┘
st ─────────────────────────────────────────────────────────────┘└─
72 rw one_mul,
id └─────┘
src └─┘└─────┘
typ └─┘└─────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────┘└─
73 exact le_max_right _ _
id └──────────┘
src └────┘└──────────┘└───┘
typ └────┘└──────────┘└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └──┘┴
st ────────────────────────┘
74 end
st └─┘
75
76 variables { f g : E → F }
77
78 lemma smul (c : 𝕜) (hf : is_bounded_linear_map 𝕜 f) :
id ┴ └───────────────────┘ ┴ ┴
src └───────────────────┘
typ ┴ └───────────────────┘ ┴ ┴
doc └───────────────────┘
79 is_bounded_linear_map 𝕜 (λ e, c • f e) :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────────┘
80 let ⟨hlf, M, hMp, hM⟩ := hf in
id └─┘ └─┘ ┴ └┘ └┘
typ └─┘ └─┘ ┴ └┘ └┘
81 (c • hlf.mk' f).is_linear.with_bound (∥c∥ * M) $ assume x,
id ┴ ┴ └──┘ ┴ └───────┘ └────────┘ ┴┴┴ ┴ ┴
src ┴ └──┘ └───────┘ └────────┘ ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ └───────┘ └────────┘ ┴┴┴ ┴ ┴
82 calc ∥c • f x∥ = ∥c∥ * ∥f x∥ : norm_smul c (f x)
id ┴┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴┴ ┴┴ └───────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
typ ┴┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴┴ ┴┴ └───────┘ ┴ ┴ ┴
83 ... ≤ ∥c∥ * (M * ∥x∥) : mul_le_mul_of_nonneg_left (hM _) (norm_nonneg _)
id ┴┴┴ ┴ ┴ ┴┴┴ └───────────────────────┘ └─────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ └───────────────────────┘ └─────────┘
typ ┴┴┴ ┴ ┴ ┴┴┴ └───────────────────────┘ └─────────┘
84 ... = (∥c∥ * M) * ∥x∥ : (mul_assoc _ _ _).symm
id ┴┴┴ ┴ ┴ ┴┴┴ └───────┘ └──┘
src ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └──┘
typ ┴┴┴ ┴ ┴ ┴┴┴ └───────┘ └──┘
85
86 lemma neg (hf : is_bounded_linear_map 𝕜 f) :
id └───────────────────┘ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴
doc └───────────────────┘
87 is_bounded_linear_map 𝕜 (λ e, -f e) :=
id └───────────────────┘ ┴ ┴ ┴┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴┴ ┴
doc └───────────────────┘
88 begin
st └─────
89 rw show (λ e, -f e) = (λ e, (-1 : 𝕜) • f e), { funext, simp },
id ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └──┘┴ ┴ └┘┴┴ └──┘ └──┘ └┘┴┴ ┴ └───┘└────┘└┘└───┘┴
typ └─┘ ┴ └──┘┴ ┴ └┘┴┴ └──┘ └──┘┴└┘┴┴┴┴ └───┘└────┘└┘└───┘┴
doc └─┘ ┴ └──┘ ┴ └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ └───┘└────┘└┘└───┘┴
txt └─┘ ┴ └──┘ ┴ └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ └───┘└────┘└┘└───┘┴
par └─┘ ┴ └──┘ ┴ └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ └───┘└────┘└┘└───┘┴
pid ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ └─────────────────┘
st ───────────────────────────────────────────────┘└─────┘└─────┘└┘└
90 exact smul (-1) hf
id └──┘ └┘
src └────┘└──┘┴ └─┘ ┴
typ └────┘└──┘┴ └─┘└┘┴
doc └────┘ ┴ └─┘ ┴
txt └────┘ ┴ └─┘ ┴
par └────┘ ┴ └─┘ ┴
pid ┴ ┴ └─┘ ┴
st ────────────────────┘
91 end
st └─┘
92
93 lemma add (hf : is_bounded_linear_map 𝕜 f) (hg : is_bounded_linear_map 𝕜 g) :
id └───────────────────┘ ┴ ┴ └───────────────────┘ ┴ ┴
src └───────────────────┘ └───────────────────┘
typ └───────────────────┘ ┴ ┴ └───────────────────┘ ┴ ┴
doc └───────────────────┘ └───────────────────┘
94 is_bounded_linear_map 𝕜 (λ e, f e + g e) :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────────┘
95 let ⟨hlf, Mf, hMfp, hMf⟩ := hf in
id └─┘ └─┘ └┘ └─┘ └┘
typ └─┘ └─┘ └┘ └─┘ └┘
96 let ⟨hlg, Mg, hMgp, hMg⟩ := hg in
id └─┘ └─┘ └┘ └─┘ └┘
typ └─┘ └─┘ └┘ └─┘ └┘
97 (hlf.mk' _ + hlg.mk' _).is_linear.with_bound (Mf + Mg) $ assume x,
id └──┘ ┴ └──┘ └───────┘ └────────┘ ┴ ┴
src └──┘ ┴ └──┘ └───────┘ └────────┘ ┴
typ └──┘ ┴ └──┘ └───────┘ └────────┘ ┴ ┴
98 calc ∥f x + g x∥ ≤ Mf * ∥x∥ + Mg * ∥x∥ : norm_add_le_of_le (hMf x) (hMg x)
id ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴ └───────────────┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴ └───────────────┘ ┴ ┴
99 ... ≤ (Mf + Mg) * ∥x∥ : by rw add_mul
id ┴ ┴ ┴┴┴ └─────┘
src ┴ ┴ ┴ ┴ └─┘└─────┘└
typ ┴ ┴ ┴┴┴ └─┘└─────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └───────────
100
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
101 lemma sub (hf : is_bounded_linear_map 𝕜 f) (hg : is_bounded_linear_map 𝕜 g) :
id └───────────────────┘ ┴ ┴ └───────────────────┘ ┴ ┴
src └───────────────────┘ └───────────────────┘
typ └───────────────────┘ ┴ ┴ └───────────────────┘ ┴ ┴
doc └───────────────────┘ └───────────────────┘
102 is_bounded_linear_map 𝕜 (λ e, f e - g e) := add hf (neg hg)
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ └─┘ └┘
src └───────────────────┘ ┴ └─┘ └─┘
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ └─┘ └┘
doc └───────────────────┘
103
104 lemma comp {g : F → G}
id ┴ ┴
typ ┴ ┴
105 (hg : is_bounded_linear_map 𝕜 g) (hf : is_bounded_linear_map 𝕜 f) :
id └───────────────────┘ ┴ ┴ └───────────────────┘ ┴ ┴
src └───────────────────┘ └───────────────────┘
typ └───────────────────┘ ┴ ┴ └───────────────────┘ ┴ ┴
doc └───────────────────┘ └───────────────────┘
106 is_bounded_linear_map 𝕜 (g ∘ f) :=
id └───────────────────┘ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴
doc └───────────────────┘
107 let ⟨hlg, Mg, hMgp, hMg⟩ := hg in
id └─┘ └─┘ └┘ └──┘ └─┘ └┘
typ └─┘ └─┘ └┘ └──┘ └─┘ └┘
108 let ⟨hlf, Mf, hMfp, hMf⟩ := hf in
id └─┘ └─┘ └┘ └─┘ └┘
typ └─┘ └─┘ └┘ └─┘ └┘
109 ((hlg.mk' _).comp (hlf.mk' _)).is_linear.with_bound (Mg * Mf) $ assume x,
id └──┘ └──┘ └──┘ └───────┘ └────────┘ ┴ ┴
src └──┘ └──┘ └──┘ └───────┘ └────────┘ ┴
typ └──┘ └──┘ └──┘ └───────┘ └────────┘ ┴ ┴
110 calc ∥g (f x)∥ ≤ Mg * ∥f x∥ : hMg _
id ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴
111 ... ≤ Mg * (Mf * ∥x∥) : mul_le_mul_of_nonneg_left (hMf _) (le_of_lt hMgp)
id ┴ ┴ ┴┴┴ └───────────────────────┘ └──────┘
src ┴ ┴ ┴ ┴ └───────────────────────┘ └──────┘
typ ┴ ┴ ┴┴┴ └───────────────────────┘ └──────┘
112 ... = Mg * Mf * ∥x∥ : (mul_assoc _ _ _).symm
id ┴ ┴ ┴┴┴ └───────┘ └──┘
src ┴ ┴ ┴ ┴ └───────┘ └──┘
typ ┴ ┴ ┴┴┴ └───────┘ └──┘
113
114 lemma tendsto (x : E) (hf : is_bounded_linear_map 𝕜 f) : f →_{x} (f x) :=
id ┴ └───────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
src └───────────────────┘ └─┘ ┴
typ ┴ └───────────────────┘ ┴ ┴ ┴ └─┘┴┴ ┴ ┴
doc └───────────────────┘ └─┘ ┴
115 let ⟨hf, M, hMp, hM⟩ := hf in
id └─┘ └┘ ┴ └┘ └┘
typ └─┘ └┘ ┴ └┘ └┘
116 tendsto_iff_norm_tendsto_zero.2 $
id └───────────────────────────┘┴
src └───────────────────────────┘┴
typ └───────────────────────────┘┴
117 squeeze_zero (assume e, norm_nonneg _)
id └──────────┘ ┴ └─────────┘
src └──────────┘ └─────────┘
typ └──────────┘ ┴ └─────────┘
118 (assume e,
id ┴
typ ┴
119 calc ∥f e - f x∥ = ∥hf.mk' f (e - x)∥ : by rw (hf.mk' _).map_sub e x; refl
id ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ └────┘└──────────┘ ┴ └────
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘└──────────┘┴┴┴ └────
doc └─┘ └──────────┘ ┴ └────
txt └─┘ └──────────┘ ┴ └────
par └─┘ └──────────┘ ┴ └────
pid ┴ └──────────┘ ┴ └
st └────────────────────────────────
120 ... ≤ M * ∥e - x∥ : hM (e - x))
id ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴
src ──────────────────┘ ┴ ┴ ┴ ┴ ┴
typ ──────────────────┘ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴
doc ──────────────────┘
txt ──────────────────┘
par ──────────────────┘
pid ──────────────────┘
st ──────────────────┘
121 (suffices (λ (e : E), M * ∥e - x∥) →_{x} (M * 0), by simpa,
id ┴ ┴ ┴┴ ┴ ┴┴ └─┘┴┴ ┴
src ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └───┘
typ ┴ ┴ ┴┴ ┴ ┴┴ └─┘┴┴ ┴ └───┘
doc └─┘ ┴ └───┘
txt └───┘
par └───┘
st └────┘
122 tendsto_const_nhds.mul (lim_norm _))
id └────────────────┘└──┘ └──────┘
src └────────────────┘└──┘ └──────┘
typ └────────────────┘└──┘ └──────┘
123
124 lemma continuous (hf : is_bounded_linear_map 𝕜 f) : continuous f :=
id └───────────────────┘ ┴ ┴ └────────┘ ┴
src └───────────────────┘ └────────┘
typ └───────────────────┘ ┴ ┴ └────────┘ ┴
doc └───────────────────┘ └────────┘
125 continuous_iff_continuous_at.2 $ λ _, hf.tendsto _
id └──────────────────────────┘┴ ┴ └┘└──────┘
src └──────────────────────────┘┴ └──────┘
typ └──────────────────────────┘┴ ┴ └┘└──────┘
126
127 lemma lim_zero_bounded_linear_map (hf : is_bounded_linear_map 𝕜 f) :
id └───────────────────┘ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴
doc └───────────────────┘
128 (f →_{0} 0) :=
id ┴ └─┘ ┴
src └─┘ ┴
typ ┴ └─┘ ┴
doc └─┘ ┴
129 (hf.1.mk' _).map_zero ▸ continuous_iff_continuous_at.1 hf.continuous 0
id └┘┴ └─┘ └──────┘ ┴ └──────────────────────────┘┴ └┘└─────────┘
src ┴ └─┘ └──────┘ ┴ └──────────────────────────┘┴ └─────────┘
typ └┘┴ └─┘ └──────┘ ┴ └──────────────────────────┘┴ └┘└─────────┘
130
131 section
132 open asymptotics filter
133
134 theorem is_O_id {f : E → F} (h : is_bounded_linear_map 𝕜 f) (l : filter E) :
id ┴ ┴ └───────────────────┘ ┴ ┴ └────┘ ┴
src └───────────────────┘ └────┘
typ ┴ ┴ └───────────────────┘ ┴ ┴ └────┘ ┴
doc └───────────────────┘
135 is_O f (λ x, x) l :=
id └──┘ ┴ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴ ┴
doc └──┘
136 let ⟨M, hMp, hM⟩ := h.bound in
id └─┘ ┴ └┘ ┴└────┘
src └────┘
typ └─┘ ┴ └┘ ┴└────┘
137 ⟨M, mem_sets_of_superset univ_mem_sets (λ x _, hM x)⟩
id └──────────────────┘ └───────────┘ ┴ ┴ ┴
src └──────────────────┘ └───────────┘
typ └──────────────────┘ └───────────┘ ┴ ┴ ┴
138
139 theorem is_O_comp {E : Type*} {g : F → G} (hg : is_bounded_linear_map 𝕜 g)
id ┴ ┴ └───────────────────┘ ┴ ┴
src └───────────────────┘
typ ┴ ┴ └───────────────────┘ ┴ ┴
doc └───────────────────┘
140 {f : E → F} (l : filter E) : is_O (λ x', g (f x')) f l :=
id ┴ ┴ └────┘ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴
src └────┘ └──┘
typ ┴ ┴ └────┘ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
141 (hg.is_O_id ⊤).comp_tendsto lattice.le_top
id └┘└──────┘ ┴ └──────────┘ └────────────┘
src └──────┘ ┴ └──────────┘ └────────────┘
typ └┘└──────┘ ┴ └──────────┘ └────────────┘
142
143 theorem is_O_sub {f : E → F} (h : is_bounded_linear_map 𝕜 f)
id ┴ ┴ └───────────────────┘ ┴ ┴
src └───────────────────┘
typ ┴ ┴ └───────────────────┘ ┴ ┴
doc └───────────────────┘
144 (l : filter E) (x : E) : is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
id └────┘ ┴ ┴ └──┘ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴
src └────┘ └──┘ ┴ ┴
typ └────┘ ┴ ┴ └──┘ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴
doc └──┘
145 is_O_comp h l
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
146
147 end
148
149 end is_bounded_linear_map
150
151 section
152 set_option class.instance_max_depth 240
doc └──────────────────────┘
153
154 lemma is_bounded_linear_map_prod_iso :
155 is_bounded_linear_map 𝕜 (λ(p : (E →L[𝕜] F) × (E →L[𝕜] G)),
id └───────────────────┘ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴
src └───────────────────┘ └─┘ ┴ ┴ └─┘ ┴
typ └───────────────────┘ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴
doc └───────────────────┘ └─┘ ┴ └─┘ ┴
156 (continuous_linear_map.prod p.1 p.2 : (E →L[𝕜] (F × G)))) :=
id └────────────────────────┘ ┴┴ ┴┴ ┴ └─┘┴┴ ┴ ┴ ┴
src └────────────────────────┘ ┴ ┴ └─┘ ┴ ┴
typ └────────────────────────┘ ┴┴ ┴┴ ┴ └─┘┴┴ ┴ ┴ ┴
doc └────────────────────────┘ └─┘ ┴
157 begin
st └─────
158 refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ 1 (λp, _),
id └──────────────────────┘ └─┘
src └─────┘└──────────────────────┘┴ └───┘ └┘ └───┘└─┘└──┘ └───┘
typ └─────┘└──────────────────────┘┴ └───┘ └┘ └───┘└─┘└──┘ └───┘
doc └─────┘ ┴ └───┘ └┘ └───┘ └──┘ └───┘
txt └─────┘ ┴ └───┘ └┘ └───┘ └──┘ └───┘
par └─────┘ ┴ └───┘ └┘ └───┘ └──┘ └───┘
pid ┴ ┴ └───┘ └┘ └───┘ └──┘ └───┘
st ─────────────────────────────────────────────────────────────────┘└─
159 simp only [norm, one_mul],
id └─────┘
src └─────────┘ └┘└─────┘┴
typ └─────────┘ └┘└─────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ──────────────────────────┘└─
160 refine continuous_linear_map.op_norm_le_bound _ (le_trans (norm_nonneg _) (le_max_left _ _)) (λu, _),
id └────────────────────────────────────┘ └──────┘ └─────────┘ └─────────┘
src └─────┘└────────────────────────────────────┘└─┘ └──────┘┴ └─────────┘└──┘ └─────────┘└─────┘ └───┘
typ └─────┘└────────────────────────────────────┘└─┘ └──────┘┴ └─────────┘└──┘ └─────────┘└─────┘ └───┘
doc └─────┘└────────────────────────────────────┘└─┘ ┴ └──┘ └─────┘ └───┘
txt └─────┘ └─┘ ┴ └──┘ └─────┘ └───┘
par └─────┘ └─┘ ┴ └──┘ └─────┘ └───┘
pid ┴ └─┘ ┴ └──┘ └─────┘ └───┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
161 simp only [norm, continuous_linear_map.prod, max_le_iff],
id └────────────────────────┘ └────────┘
src └─────────┘ └┘└────────────────────────┘└┘└────────┘┴
typ └─────────┘ └┘└────────────────────────┘└┘└────────┘┴
doc └─────────┘ └┘└────────────────────────┘└┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────┘└─
162 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
163 { calc ∥p.1 u∥ ≤ ∥p.1∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
id └──┘ ┴ ┴ └──────────────────────────────┘
src └──┘ ┴ ┴ └──────────────────────────────┘
typ └──┘ ┴ ┴ └──────────────────────────────┘
doc └──┘ └──────────────────────────────┘
st ───┘└─────────────────────────────────────────────────────────────────
164 ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
id └─┘ ┴┴ ┴
src └─┘ ┴
typ └─┘ ┴┴ ┴
st ──────────────────────────────────────
165 mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) },
id └────────────────────────┘ └─────────┘ └─────────┘
src └────────────────────────┘ └─────────┘ └─────────┘
typ └────────────────────────┘ └─────────┘ └─────────┘
st ─────────────────────────────────────────────────────────────────┘└─┘└
166 { calc ∥p.2 u∥ ≤ ∥p.2∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
id └──┘ └──────────────────────────────┘
src └──┘ └──────────────────────────────┘
typ └──┘ └──────────────────────────────┘
doc └──┘ └──────────────────────────────┘
st ──────────────────────────────────────────────────────────────────────
167 ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
st ──────────────────────────────────────
168 mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg _) }
id └────────────────────────┘ └──────────┘ └─────────┘
src └────────────────────────┘ └──────────┘ └─────────┘
typ └────────────────────────┘ └──────────┘ └─────────┘
st ──────────────────────────────────────────────────────────────────┘└──
169 end
st ──┘
170
171 lemma continuous_linear_map.is_bounded_linear_map_comp_left (g : continuous_linear_map 𝕜 F G) :
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
172 is_bounded_linear_map 𝕜 (λ(f : E →L[𝕜] F), continuous_linear_map.comp g f) :=
id └───────────────────┘ ┴ ┴ └─┘┴┴ ┴ └────────────────────────┘ ┴ ┴
src └───────────────────┘ └─┘ ┴ └────────────────────────┘
typ └───────────────────┘ ┴ ┴ └─┘┴┴ ┴ └────────────────────────┘ ┴ ┴
doc └───────────────────┘ └─┘ ┴ └────────────────────────┘
173 begin
st └─────
174 refine is_linear_map.with_bound ⟨λu v, _, λc u, _⟩
id └──────────────────────┘
src └─────┘└──────────────────────┘┴ └──────┘ └───────
typ └─────┘└──────────────────────┘┴ └──────┘ └───────
doc └─────┘ ┴ └──────┘ └───────
txt └─────┘ ┴ └──────┘ └───────
par └─────┘ ┴ └──────┘ └───────
pid ┴ ┴ └──────┘ └───────
st ─────────────────────────────────────────────────────
175 (∥g∥) (λu, continuous_linear_map.op_norm_comp_le _ _),
id ┴┴┴ └───────────────────────────────────┘
src ───┘ ┴ ┴└┘ └─┘└───────────────────────────────────┘└───┘
typ ───┘ ┴┴┴└┘ └─┘└───────────────────────────────────┘└───┘
doc ───┘ └┘ └─┘└───────────────────────────────────┘└───┘
txt ───┘ └┘ └─┘ └───┘
par ───┘ └┘ └─┘ └───┘
pid ───┘ └┘ └─┘ └───┘
st ────────────────────────────────────────────────────────┘└─
176 { ext x,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
177 change g ((u+v) x) = g (u x) + g (v x),
id ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └┘ └┘┴┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ └┘ └┘┴┴ ┴ ┴┴ └┘ ┴┴┴ ┴┴┴┴
doc └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └─────┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
178 have : (u+v) x = u x + v x := rfl,
id ┴ ┴ ┴ └─┘
src └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└─┘
typ └─────┘ └┘ ┴ ┴┴┴ ┴ ┴┴┴┴└──┘└─┘
doc └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
st ────────────────────────────────────┘└─
179 rw [this, g.map_add] },
id └──┘
src └──┘ └┘ └┘
typ └──┘└──┘└┘└───────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───────────┘└─────────┘┴┴└┘└
180 { ext x,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ────────┘└─
181 change g ((c • u) x) = c • g (u x),
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴┴┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴┴┴ └┘ └┘ ┴┴┴ ┴┴┴ ┴┴┴┴
doc └─────┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
182 have : (c • u) x = c • u x := rfl,
id ┴ ┴ ┴ └─┘
src └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘└─┘
typ └─────┘ ┴ ┴ └┘ ┴ ┴┴┴ ┴┴┴┴└──┘└─┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘
st ────────────────────────────────────┘└─
183 rw [this, continuous_linear_map.map_smul] }
id └──┘ └────────────────────────────┘
src └──┘ └┘└────────────────────────────┘└┘
typ └──┘└──┘└┘└────────────────────────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───────────┘└──────────────────────────────┘┴┴└─
184 end
st ──┘
185
186 lemma continuous_linear_map.is_bounded_linear_map_comp_right (f : continuous_linear_map 𝕜 E F) :
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
187 is_bounded_linear_map 𝕜 (λ(g : F →L[𝕜] G), continuous_linear_map.comp g f) :=
id └───────────────────┘ ┴ ┴ └─┘┴┴ ┴ └────────────────────────┘ ┴ ┴
src └───────────────────┘ └─┘ ┴ └────────────────────────┘
typ └───────────────────┘ ┴ ┴ └─┘┴┴ ┴ └────────────────────────┘ ┴ ┴
doc └───────────────────┘ └─┘ ┴ └────────────────────────┘
188 begin
st └─────
189 refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ (∥f∥) (λg, _),
id └──────────────────────┘ └─┘ ┴┴┴
src └─────┘└──────────────────────┘┴ └───┘ └┘ └───┘└─┘└┘ ┴ ┴└┘ └───┘
typ └─────┘└──────────────────────┘┴ └───┘ └┘ └───┘└─┘└┘ ┴┴┴└┘ └───┘
doc └─────┘ ┴ └───┘ └┘ └───┘ └┘ └┘ └───┘
txt └─────┘ ┴ └───┘ └┘ └───┘ └┘ └┘ └───┘
par └─────┘ ┴ └───┘ └┘ └───┘ └┘ └┘ └───┘
pid ┴ ┴ └───┘ └┘ └───┘ └┘ └┘ └───┘
st ─────────────────────────────────────────────────────────────────────┘└─
190 rw mul_comm,
id └──────┘
src └─┘└──────┘
typ └─┘└──────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────┘└─
191 exact continuous_linear_map.op_norm_comp_le _ _
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘└───┘
typ └────┘└───────────────────────────────────┘└───┘
doc └────┘└───────────────────────────────────┘└───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └──┘┴
st ─────────────────────────────────────────────────┘
192 end
st └─┘
193
194 end
195
196 section bilinear_map
197
198 variable (𝕜)
199
200 /-- A map `f : E × F → G` satisfies `is_bounded_bilinear_map 𝕜 f` if it is bilinear and
201 continuous. -/
202 structure is_bounded_bilinear_map (f : E × F → G) : Prop :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
203 (add_left : ∀(x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y))
id ┴ ┴ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘ ┴
204 (smul_left : ∀(c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x,y))
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
205 (add_right : ∀(x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂))
id ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ └┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴ └┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴┴ └┘
206 (smul_right : ∀(c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x,y))
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
207 (bound : ∃C>0, ∀(x : E) (y : F), ∥f (x, y)∥ ≤ C * ∥x∥ * ∥y∥)
id ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
208
209 variable {𝕜}
210 variable {f : E × F → G}
id ┴
src ┴
typ ┴
211
212 lemma is_bounded_bilinear_map.map_sub_left (h : is_bounded_bilinear_map 𝕜 f) {x y : E} {z : F} :
id └─────────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴ ┴ ┴ ┴
doc └─────────────────────┘
213 f (x - y, z) = f (x, z) - f(y, z) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴
214 calc f (x - y, z) = f (x + (-1 : 𝕜) • y, z) : by simp
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └───┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
215 ... = f (x, z) + (-1 : 𝕜) • f (y, z) : by simp only [h.add_left, h.smul_left]
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ └─────────┘ └┘ └┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────────┘└────────┘└┘└─────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st └───────────────────────────────────┘
216 ... = f (x, z) - f (y, z) : by simp
id ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ └────
typ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
217
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
218 lemma is_bounded_bilinear_map.map_sub_right (h : is_bounded_bilinear_map 𝕜 f) {x : E} {y z : F} :
id └─────────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴ ┴ ┴ ┴
doc └─────────────────────┘
219 f (x, y - z) = f (x, y) - f (x, z) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
220 calc f (x, y - z) = f (x, y + (-1 : 𝕜) • z) : by simp
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └───┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
221 ... = f (x, y) + (-1 : 𝕜) • f (x, z) : by simp only [h.add_right, h.smul_right]
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ └─────────┘ └┘ └┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─────────┘└─────────┘└┘└──────────┘└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st └─────────────────────────────────────┘
222 ... = f (x, y) - f (x, z) : by simp
id ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ └────
typ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
223
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
224 lemma is_bounded_bilinear_map_smul :
225 is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × E), p.1 • p.2) :=
id └─────────────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └─────────────────────┘ ┴ ┴ ┴ ┴
typ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └─────────────────────┘
226 { add_left := add_smul,
id └──────┘
src └──────┘
typ └──────┘
227 smul_left := λc x y, by simp [smul_smul],
id ┴ ┴ ┴ └───────┘
src └────┘└───────┘┴
typ ┴ ┴ ┴ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────┘
228 add_right := smul_add,
id └──────┘
src └──────┘
typ └──────┘
229 smul_right := λc x y, by simp [smul_smul, mul_comm],
id ┴ ┴ ┴ └───────┘ └──────┘
src └────┘└───────┘└┘└──────┘┴
typ ┴ ┴ ┴ └────┘└───────┘└┘└──────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────────────┘
230 bound := ⟨1, zero_lt_one, λx y, by simp [norm_smul]⟩ }
id └─────────┘ ┴ ┴ └───────┘
src └─────────┘ └────┘└───────┘┴
typ └─────────┘ ┴ ┴ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────┘
231
232 lemma is_bounded_bilinear_map_mul :
233 is_bounded_bilinear_map 𝕜 (λ (p : 𝕜 × 𝕜), p.1 * p.2) :=
id └─────────────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └─────────────────────┘ ┴ ┴ ┴ ┴
typ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └─────────────────────┘
234 is_bounded_bilinear_map_smul
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
235
236 lemma is_bounded_bilinear_map_comp :
237 is_bounded_bilinear_map 𝕜 (λ(p : (E →L[𝕜] F) × (F →L[𝕜] G)), p.2.comp p.1) :=
id └─────────────────────┘ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ └──┘ ┴┴
src └─────────────────────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴
typ └─────────────────────┘ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ └──┘ ┴┴
doc └─────────────────────┘ └─┘ ┴ └─┘ ┴ └──┘
238 { add_left := λx₁ x₂ y, begin
id └┘ └┘ ┴
typ └┘ └┘ ┴
st └─────
239 ext z,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────────┘└─
240 change y (x₁ z + x₂ z) = y (x₁ z) + y (x₂ z),
id ┴ ┴ └┘ ┴ └┘ ┴
src └─────┘ ┴ ┴ ┴┴┴ ┴ └┘┴┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴┴┴ ┴ └┘┴┴ ┴ └┘┴ └┘ ┴┴┴ └┘┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────┘└─
241 rw y.map_add
src └─┘ └
typ └─┘└───────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ───────────────────
242 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
243 smul_left := λc x y, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └─────
244 ext z,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────────┘└─
245 change y (c • (x z)) = c • y (x z),
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴┴┴ ┴ └─┘ ┴┴┴ ┴┴┴ ┴┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
246 rw continuous_linear_map.map_smul
id └────────────────────────────┘
src └─┘└────────────────────────────┘└
typ └─┘└────────────────────────────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ────────────────────────────────────────
247 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
248 add_right := λx y₁ y₂, rfl,
id ┴ └┘ └┘ └─┘
src └─┘
typ ┴ └┘ └┘ └─┘
249 smul_right := λc x y, rfl,
id ┴ ┴ ┴ └─┘
src └─┘
typ ┴ ┴ ┴ └─┘
250 bound := ⟨1, zero_lt_one, λx y, calc
id └─────────┘ ┴ ┴
src └─────────┘
typ └─────────┘ ┴ ┴
251 ∥continuous_linear_map.comp ((x, y).snd) ((x, y).fst)∥
id ┴└────────────────────────┘ ┴┴ ┴ └─┘ ┴┴ ┴ └─┘ ┴
src ┴└────────────────────────┘ ┴ └─┘ ┴ └─┘ ┴
typ ┴└────────────────────────┘ ┴┴ ┴ └─┘ ┴┴ ┴ └─┘ ┴
doc └────────────────────────┘
252 ≤ ∥y∥ * ∥x∥ : continuous_linear_map.op_norm_comp_le _ _
id ┴┴┴ ┴ ┴┴┴ └───────────────────────────────────┘
src ┴ ┴ ┴ ┴ ┴ └───────────────────────────────────┘
typ ┴┴┴ ┴ ┴┴┴ └───────────────────────────────────┘
doc └───────────────────────────────────┘
253 ... = 1 * ∥x∥ * ∥ y∥ : by ring ⟩ }
id ┴ ┴┴┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ └───┘
typ ┴ ┴┴┴ ┴ ┴ ┴┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
254
255 lemma is_bounded_bilinear_map_apply :
256 is_bounded_bilinear_map 𝕜 (λp : (E →L[𝕜] F) × E, p.1 p.2) :=
id └─────────────────────┘ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ ┴┴ ┴┴
src └─────────────────────┘ └─┘ ┴ ┴ ┴ ┴
typ └─────────────────────┘ ┴ ┴ └─┘┴┴ ┴ ┴ ┴ ┴┴ ┴┴
doc └─────────────────────┘ └─┘ ┴
257 { add_left := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
258 smul_left := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
259 add_right := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
260 smul_right := by simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
261 bound := ⟨1, zero_lt_one, by simp [continuous_linear_map.le_op_norm]⟩ }
id └─────────┘ └──────────────────────────────┘
src └─────────┘ └────┘└──────────────────────────────┘┴
typ └─────────┘ └────┘└──────────────────────────────┘┴
doc └────┘└──────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └──────────────────────────────────────┘
262
263 /-- The function `continuous_linear_map.smul_right`, associating to a continuous linear map
264 `f : E → 𝕜` and a scalar `c : F` the tensor product `f ⊗ c` as a continuous linear map from `E` to
265 `F`, is a bounded bilinear map. -/
266 lemma is_bounded_bilinear_map_smul_right :
267 is_bounded_bilinear_map 𝕜
id └─────────────────────┘ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴
doc └─────────────────────┘
268 (λp, (continuous_linear_map.smul_right : (E →L[𝕜] 𝕜) → F → (E →L[𝕜] F)) p.1 p.2) :=
id ┴ └──────────────────────────────┘ ┴ └─┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴┴
src └──────────────────────────────┘ └─┘ ┴ └─┘ ┴ ┴ ┴
typ ┴ └──────────────────────────────┘ ┴ └─┘┴┴ ┴ ┴ ┴ └─┘┴┴ ┴ ┴┴ ┴┴
doc └──────────────────────────────┘ └─┘ ┴ └─┘ ┴
269 { add_left := λm₁ m₂ f, by { ext z, simp [add_smul] },
id └┘ └┘ ┴ └──────┘
src └───┘ └────┘└──────┘└┘
typ └┘ └┘ ┴ └───┘ └────┘└──────┘└┘
doc └───┘ └────┘ └┘
txt └───┘ └────┘ └┘
par └───┘ └────┘ └┘
pid └┘ ┴┴ ┴┴
st └──────┘└────────────────┘└┘
270 smul_left := λc m f, by { ext z, simp [mul_smul] },
id ┴ ┴ ┴ └──────┘
src └───┘ └────┘└──────┘└┘
typ ┴ ┴ ┴ └───┘ └────┘└──────┘└┘
doc └───┘ └────┘ └┘
txt └───┘ └────┘ └┘
par └───┘ └────┘ └┘
pid └┘ ┴┴ ┴┴
st └──────┘└────────────────┘└┘
271 add_right := λm f₁ f₂, by { ext z, simp [smul_add] },
id ┴ └┘ └┘ └──────┘
src └───┘ └────┘└──────┘└┘
typ ┴ └┘ └┘ └───┘ └────┘└──────┘└┘
doc └───┘ └────┘ └┘
txt └───┘ └────┘ └┘
par └───┘ └────┘ └┘
pid └┘ ┴┴ ┴┴
st └──────┘└────────────────┘└┘
272 smul_right := λc m f, by { ext z, simp [smul_smul, mul_comm] },
id ┴ ┴ ┴ └───────┘ └──────┘
src └───┘ └────┘└───────┘└┘└──────┘└┘
typ ┴ ┴ ┴ └───┘ └────┘└───────┘└┘└──────┘└┘
doc └───┘ └────┘ └┘ └┘
txt └───┘ └────┘ └┘ └┘
par └───┘ └────┘ └┘ └┘
pid └┘ ┴┴ └┘ ┴┴
st └──────┘└───────────────────────────┘└┘
273 bound := ⟨1, zero_lt_one, λm f, by simp⟩ }
id └─────────┘ ┴ ┴
src └─────────┘ └──┘
typ └─────────┘ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
274
275 /-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
276 `q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
277 We define this function here a bounded linear map from `E × F` to `G`. The fact that this
278 is indeed the derivative of `f` is proved in `is_bounded_bilinear_map.has_fderiv_at` in
279 `fderiv.lean`-/
280
281 def is_bounded_bilinear_map.linear_deriv (h : is_bounded_bilinear_map 𝕜 f) (p : E × F) :
id └─────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────────────┘ ┴
typ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────────────┘
282 (E × F) →ₗ[𝕜] G :=
id ┴ ┴ ┴ └─┘┴┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘┴┴ ┴
283 { to_fun := λq, f (p.1, q.2) + f (q.1, p.2),
id ┴ ┴ ┴┴┴ ┴┴ ┴ ┴ ┴┴┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴┴ ┴ ┴ ┴┴┴ ┴┴
284 add := λq₁ q₂, begin
id └┘ └┘
typ └┘ └┘
st └─────
285 change f (p.1, q₁.2 + q₂.2) + f (q₁.1 + q₂.1, p.2) =
id ┴ ┴
src └─────┘ ┴ └──┘ └─┘┴┴ └──┘ ┴ ┴ └─┘ ┴ └──┘ └──┘┴└
typ └─────┘ ┴ └──┘ └─┘┴┴ └──┘ ┴ ┴ └─┘ ┴ └──┘ └──┘┴└
doc └─────┘ ┴ └──┘ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └──┘ └──┘ └
txt └─────┘ ┴ └──┘ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └──┘ └──┘ └
par └─────┘ ┴ └──┘ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └──┘ └──┘ └
pid ┴ ┴ └──┘ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └──┘ └──┘ └
st ─────────────────────────────────────────────────────────
286 f (p.1, q₁.2) + f (q₁.1, p.2) + (f (p.1, q₂.2) + f (q₂.1, p.2)),
id └┘ ┴ ┴└┘ ┴
src ─────┘ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴┴ └──┘ └──┘
typ ─────┘ ┴ └──┘ └──┘ ┴ ┴ └┘└──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴┴┴┴└┘└──┘┴└──┘
doc ─────┘ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
txt ─────┘ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
par ─────┘ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
pid ─────┘ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
st ────────────────────────────────────────────────────────────────────┘└─
287 simp [h.add_left, h.add_right]
src └────┘ └┘ └─
typ └────┘└────────┘└┘└─────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ───────────────────────────────────
288 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
289 smul := λc q, begin
id ┴ ┴
typ ┴ ┴
st └─────
290 change f (p.1, c • q.2) + f (c • q.1, p.2) = c • (f (p.1, q.2) + f (q.1, p.2)),
id ┴ ┴ ┴ ┴┴ ┴
src └─────┘ ┴ └──┘ ┴┴┴ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴┴ └──┘ └──┘
typ └─────┘ ┴ └──┘ ┴┴┴ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴┴┴ ┴ ┴ └──┘ └──┘ ┴┴┴┴┴└──┘┴└──┘
doc └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
txt └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
par └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
pid ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └──┘
st ─────────────────────────────────────────────────────────────────────────────────┘└─
291 simp [h.smul_left, h.smul_right, smul_add]
id └──────┘
src └────┘ └┘ └┘└──────┘└─
typ └────┘└─────────┘└┘└──────────┘└┘└──────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st ───────────────────────────────────────────────
292 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
293
294 /-- The derivative of a bounded bilinear map at a point `p : E × F`, as a continuous linear map
295 from `E × F` to `G`. -/
296 def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map 𝕜 f) (p : E × F) : (E × F) →L[𝕜] G :=
id └─────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴
src └─────────────────────┘ ┴ ┴ └─┘ ┴
typ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴
doc └─────────────────────┘ └─┘ ┴
297 (h.linear_deriv p).mk_continuous_of_exists_bound $ begin
id ┴└───────────┘ ┴ └───────────────────────────┘
src └───────────┘ └───────────────────────────┘
typ ┴└───────────┘ ┴ └───────────────────────────┘
doc └───────────┘ └───────────────────────────┘
st └─────
298 rcases h.bound with ⟨C, Cpos, hC⟩,
id └─────┘
src └─────┘└─────┘└─────────────────┘
typ └─────┘└─────┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ──────────────────────────────────┘└─
299 refine ⟨C * ∥p.1∥ + C * ∥p.2∥, λq, _⟩,
id ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴┴┴┴ └┘┴┴┴┴ ┴ ┴ └┘ └┘ └───┘
typ └─────┘ ┴┴┴┴ └┘┴┴┴┴┴┴ ┴ ┴└┘ └┘ └───┘
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ └───┘
st ──────────────────────────────────────┘└─
300 calc ∥f (p.1, q.2) + f (q.1, p.2)∥
id └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴
doc └──┘
st ─────────────────────────────────────
301 ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
id ┴ ┴ ┴ └───────────────┘ └┘
src └───────────────┘
typ ┴ ┴ ┴ └───────────────┘ └┘
st ──────────────────────────────────────────────────────────────────────────────────
302 ... ≤ C * ∥p.1∥ * ∥q∥ + C * ∥q∥ * ∥p.2∥ : begin
st ───────────────────────────────────────────┘└─────
303 apply add_le_add,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
304 exact mul_le_mul_of_nonneg_left (le_max_right _ _) (mul_nonneg (le_of_lt Cpos) (norm_nonneg _)),
id └───────────────────────┘ └──────────┘ └────────┘ └──────┘ └──┘ └─────────┘
src └────┘└───────────────────────┘┴ └──────────┘└────┘ └────────┘┴ └──────┘┴ └┘ └─────────┘└──┘
typ └────┘└───────────────────────┘┴ └──────────┘└────┘ └────────┘┴ └──────┘┴└──┘└┘ └─────────┘└──┘
doc └────┘ ┴ └────┘ ┴ ┴ └┘ └──┘
txt └────┘ ┴ └────┘ ┴ ┴ └┘ └──┘
par └────┘ ┴ └────┘ ┴ ┴ └┘ └──┘
pid ┴ ┴ └────┘ ┴ ┴ └┘ └──┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
305 apply mul_le_mul_of_nonneg_right _ (norm_nonneg _),
id └────────────────────────┘ └─────────┘
src └────┘└────────────────────────┘└─┘ └─────────┘└─┘
typ └────┘└────────────────────────┘└─┘ └─────────┘└─┘
doc └────┘ └─┘ └─┘
txt └────┘ └─┘ └─┘
par └────┘ └─┘ └─┘
pid ┴ └─┘ └─┘
st ───────────────────────────────────────────────────────┘└─
306 exact mul_le_mul_of_nonneg_left (le_max_left _ _) (le_of_lt Cpos),
id └───────────────────────┘ └─────────┘ └──────┘ └──┘
src └────┘└───────────────────────┘┴ └─────────┘└────┘ └──────┘┴ ┴
typ └────┘└───────────────────────┘┴ └─────────┘└────┘ └──────┘┴└──┘┴
doc └────┘ ┴ └────┘ ┴ ┴
txt └────┘ ┴ └────┘ ┴ ┴
par └────┘ ┴ └────┘ ┴ ┴
pid ┴ ┴ └────┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────┘└─
307 end
st ────┘└
308 ... = (C * ∥p.1∥ + C * ∥p.2∥) * ∥q∥ : by ring
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────────────────────────────────────────┘└────┘
309 end
st └─┘
310
311 @[simp] lemma is_bounded_bilinear_map_deriv_coe (h : is_bounded_bilinear_map 𝕜 f) (p q : E × F) :
id └─────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────────────┘ ┴
typ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────────────────┘
312 h.deriv p q = f (p.1, q.2) + f (q.1, p.2) := rfl
id ┴└────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴ ┴ ┴ ┴┴┴ ┴┴ └─┘
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴└────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴ ┴ ┴ ┴┴┴ ┴┴ └─┘
doc └────┘
313
314 set_option class.instance_max_depth 100
doc └──────────────────────┘
315
316 /-- Given a bounded bilinear map `f`, the map associating to a point `p` the derivative of `f` at
317 `p` is itself a bounded linear map. -/
318 lemma is_bounded_bilinear_map.is_bounded_linear_map_deriv (h : is_bounded_bilinear_map 𝕜 f) :
id └─────────────────────┘ ┴ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴ ┴
doc └─────────────────────┘
319 is_bounded_linear_map 𝕜 (λp : E × F, h.deriv p) :=
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴
src └───────────────────┘ ┴ └────┘
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴
doc └───────────────────┘ └────┘
320 begin
st └─────
321 rcases h.bound with ⟨C, Cpos, hC⟩,
id └─────┘
src └─────┘└─────┘└─────────────────┘
typ └─────┘└─────┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ──────────────────────────────────┘└─
322 refine is_linear_map.with_bound ⟨λp₁ p₂, _, λc p, _⟩ (C + C) (λp, _),
id └──────────────────────┘ ┴ ┴
src └─────┘└──────────────────────┘┴ └────────┘ └──────┘ ┴┴┴ └┘ └───┘
typ └─────┘└──────────────────────┘┴ └────────┘ └──────┘ ┴┴┴┴└┘ └───┘
doc └─────┘ ┴ └────────┘ └──────┘ ┴ ┴ └┘ └───┘
txt └─────┘ ┴ └────────┘ └──────┘ ┴ ┴ └┘ └───┘
par └─────┘ ┴ └────────┘ └──────┘ ┴ ┴ └┘ └───┘
pid ┴ ┴ └────────┘ └──────┘ ┴ ┴ └┘ └───┘
st ─────────────────────────────────────────────────────────────────────┘└─
323 { ext q,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
324 simp [h.add_left, h.add_right] },
src └────┘ └┘ └┘
typ └────┘└────────┘└┘└─────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ──────────────────────────────────┘└┘└
325 { ext q,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
326 simp [h.smul_left, h.smul_right, smul_add] },
id └──────┘
src └────┘ └┘ └┘└──────┘└┘
typ └────┘└─────────┘└┘└──────────┘└┘└──────┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ──────────────────────────────────────────────┘└┘└
327 { refine continuous_linear_map.op_norm_le_bound _
id └────────────────────────────────────┘
src └─────┘└────────────────────────────────────┘└──
typ └─────┘└────────────────────────────────────┘└──
doc └─────┘└────────────────────────────────────┘└──
txt └─────┘ └──
par └─────┘ └──
pid ┴ └──
st ────────────────────────────────────────────────────
328 (mul_nonneg (add_nonneg (le_of_lt Cpos) (le_of_lt Cpos)) (norm_nonneg _)) (λq, _),
id └────────┘ └────────┘ └──────┘ └──┘ └─────────┘
src ─────┘ └────────┘┴ └────────┘┴ ┴ └┘ └──────┘┴ └─┘ └─────────┘└───┘ └───┘
typ ─────┘ └────────┘┴ └────────┘┴ ┴ └┘ └──────┘┴└──┘└─┘ └─────────┘└───┘ └───┘
doc ─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └───┘ └───┘
txt ─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └───┘ └───┘
par ─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └───┘ └───┘
pid ─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └───┘ └───┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
329 calc ∥f (p.1, q.2) + f (q.1, p.2)∥
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
st ───────────────────────────────────────
330 ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
id ┴ ┴ ┴ └───────────────┘ └┘
src └───────────────┘
typ ┴ ┴ ┴ └───────────────┘ └┘
st ────────────────────────────────────────────────────────────────────────────────────
331 ... ≤ C * ∥p∥ * ∥q∥ + C * ∥q∥ * ∥p∥ : by apply_rules [add_le_add, mul_le_mul, norm_nonneg,
id ┴ └────────┘ └────────┘ └─────────┘
src ┴ └───────────┘└────────┘└┘└────────┘└┘└─────────┘└─
typ ┴ └───────────┘└────────┘└┘└────────┘└┘└─────────┘└─
doc └───────────┘ └┘ └┘ └─
txt └───────────┘ └┘ └┘ └─
par └───────────┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st ───────────────────────────────────────────┘└──────────────────────────────────────────────────
332 le_of_lt Cpos, le_refl, le_max_left, le_max_right, mul_nonneg, norm_nonneg, norm_nonneg,
id └──────┘ └──┘ └─────┘ └─────────┘ └──────────┘ └────────┘ └─────────┘ └─────────┘
src ─────┘└──────┘┴ └┘└─────┘└┘└─────────┘└┘└──────────┘└┘└────────┘└┘└─────────┘└┘└─────────┘└─
typ ─────┘└──────┘┴└──┘└┘└─────┘└┘└─────────┘└┘└──────────┘└┘└────────┘└┘└─────────┘└┘└─────────┘└─
doc ─────┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └─
txt ─────┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └─
par ─────┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └─
pid ─────┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────────────────────────────────────────────
333 norm_nonneg]
id └─────────┘
src ─────┘└─────────┘└─
typ ─────┘└─────────┘└─
doc ─────┘ └─
txt ─────┘ └─
par ─────┘ └─
pid ─────┘ ┴└
st ───────────────────
334 ... = (C + C) * ∥p∥ * ∥q∥ : by ring },
src ───┘ └───┘
typ ───┘ └───┘
doc ───┘ └───┘
txt ───┘ └───┘
par ───┘ └───┘
pid ───┘ ┴
st ───┘└────────────────────────────┘└────┘└──
335 end
st ──┘
336
337 end bilinear_map